(set-logic QF_AUFBV)
(set-info :source |These benchmarks are derived from a semi-automated proof of functional equivalence between two implementations of an Elliptic Curve Digital Signature Algorithm (ECDSA). More information about problem they encode can be found here: http://cps-vo.org/node/3405|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x166 () (_ BitVec 1))
(declare-fun x164 () (_ BitVec 1))
(declare-fun x162 () (_ BitVec 1))
(declare-fun x160 () (_ BitVec 1))
(declare-fun x158 () (_ BitVec 1))
(declare-fun x157 () (_ BitVec 1))
(declare-fun x156 () (_ BitVec 384))
(declare-fun x155 () (_ BitVec 1))
(declare-fun x153 () (_ BitVec 1))
(declare-fun x152 () (_ BitVec 1))
(declare-fun x151 () (_ BitVec 384))
(declare-fun x149 () (_ BitVec 1))
(declare-fun x147 () (_ BitVec 1))
(declare-fun x146 () (_ BitVec 1))
(declare-fun x144 () (_ BitVec 1))
(declare-fun x142 () (_ BitVec 1))
(declare-fun x140 () (_ BitVec 1))
(declare-fun x138 () (_ BitVec 1))
(declare-fun x136 () (_ BitVec 1))
(declare-fun x135 () (_ BitVec 1))
(declare-fun x134 () (_ BitVec 384))
(declare-fun x133 () (_ BitVec 1))
(declare-fun x131 () (_ BitVec 1))
(declare-fun x129 () (_ BitVec 1))
(declare-fun x128 () (_ BitVec 1))
(declare-fun x127 () (_ BitVec 384))
(declare-fun x126 () (_ BitVec 384))
(declare-fun x125 () (_ BitVec 1))
(declare-fun x123 () (_ BitVec 1))
(declare-fun x121 () (_ BitVec 1))
(declare-fun x119 () (_ BitVec 1))
(declare-fun x117 () (_ BitVec 1))
(declare-fun x115 () (_ BitVec 1))
(declare-fun x114 () (_ BitVec 1))
(declare-fun x113 () (_ BitVec 384))
(declare-fun x112 () (_ BitVec 1))
(declare-fun x110 () (_ BitVec 1))
(declare-fun x108 () (_ BitVec 1))
(declare-fun x107 () (_ BitVec 1))
(declare-fun x106 () (_ BitVec 384))
(declare-fun x105 () (_ BitVec 1152))
(declare-fun x104 () (_ BitVec 768))
(declare-fun x103 () (_ BitVec 384))
(declare-fun x102 ((_ BitVec 384) (_ BitVec 384) (_ BitVec 384)) (_ BitVec 384))
(declare-fun x101 () (_ BitVec 384))
(declare-fun x100 () (_ BitVec 384))
(declare-fun x99 () (_ BitVec 384))
(declare-fun x98 () (_ BitVec 384))
(declare-fun x97 () (_ BitVec 1152))
(declare-fun x96 ((_ BitVec 384) (_ BitVec 768)) (_ BitVec 1152))
(declare-fun x95 () (_ BitVec 768))
(declare-fun x94 () (_ BitVec 384))
(declare-fun x93 () (_ BitVec 384))
(declare-fun x92 () (_ BitVec 384))
(declare-fun x91 ((_ BitVec 384) (_ BitVec 384) (_ BitVec 384)) (_ BitVec 384))
(declare-fun x90 () (_ BitVec 384))
(declare-fun x89 () (_ BitVec 384))
(declare-fun x88 () (_ BitVec 384))
(declare-fun x86 () (_ BitVec 1))
(declare-fun x84 () (_ BitVec 1))
(declare-fun x82 () (_ BitVec 1))
(declare-fun x80 () (_ BitVec 1))
(declare-fun x79 () (_ BitVec 1))
(declare-fun x77 () (_ BitVec 1))
(declare-fun x75 () (_ BitVec 1))
(declare-fun x73 () (_ BitVec 1))
(declare-fun x72 () (_ BitVec 1))
(declare-fun x71 () (_ BitVec 1))
(declare-fun x69 () (_ BitVec 1))
(declare-fun x67 () (_ BitVec 1))
(declare-fun x66 () (_ BitVec 1))
(declare-fun x64 () (_ BitVec 1))
(declare-fun x63 () (_ BitVec 1))
(declare-fun x62 () (_ BitVec 384))
(declare-fun x61 () (_ BitVec 384))
(declare-fun x59 () (_ BitVec 1))
(declare-fun x58 () (_ BitVec 1))
(declare-fun x57 () (_ BitVec 384))
(declare-fun x56 () (_ BitVec 384))
(declare-fun x55 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x54 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x53 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x52 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x51 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x50 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x49 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x48 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x47 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x46 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x45 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x44 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x43 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x42 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x41 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x40 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x39 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x38 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x37 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x36 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x35 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x34 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x33 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x32 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x31 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x30 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x29 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x28 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x27 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x26 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x25 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x24 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x23 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x22 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x21 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x20 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x19 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x18 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x17 () (Array (_ BitVec 5) (_ BitVec 32)))
(declare-fun x16 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x15 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x14 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x13 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x12 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x11 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x10 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x9 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x8 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x7 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x6 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x5 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x4 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x3 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x2 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x1 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x0 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun p167 () Bool)
(declare-fun p165 () Bool)
(declare-fun p163 () Bool)
(declare-fun p161 () Bool)
(declare-fun p159 () Bool)
(declare-fun p154 () Bool)
(declare-fun p150 () Bool)
(declare-fun p148 () Bool)
(declare-fun p145 () Bool)
(declare-fun p143 () Bool)
(declare-fun p141 () Bool)
(declare-fun p139 () Bool)
(declare-fun p137 () Bool)
(declare-fun p132 () Bool)
(declare-fun p130 () Bool)
(declare-fun p124 () Bool)
(declare-fun p122 () Bool)
(declare-fun p120 () Bool)
(declare-fun p118 () Bool)
(declare-fun p116 () Bool)
(declare-fun p111 () Bool)
(declare-fun p109 () Bool)
(declare-fun p87 () Bool)
(declare-fun p85 () Bool)
(declare-fun p83 () Bool)
(declare-fun p81 () Bool)
(declare-fun p78 () Bool)
(declare-fun p76 () Bool)
(declare-fun p74 () Bool)
(declare-fun p70 () Bool)
(declare-fun p68 () Bool)
(declare-fun p65 () Bool)
(declare-fun p60 () Bool)
(assert (= p167 (and p145 p165)))
(assert (= x166 (bvand x144 x164)))
(assert (= p165 (or (= x56 x57) p163)))
(assert (= x164 (bvor x146 x162)))
(assert (= p163 (or p148 p161)))
(assert (= x162 (bvor x147 x160)))
(assert (= p161 (and p154 p159)))
(assert (= x160 (bvand x153 x158)))
(assert (= p159 (or (= x61 x62) (= (_ bv0 384) x156))))
(assert (= x158 (bvor x155 x157)))
(assert (= x157 (ite (= (_ bv0 384) x156) (_ bv1 1) (_ bv0 1))))
(assert (= x156 ((_ extract 1151 768) x97)))
(assert (= x155 (ite (= x61 x62) (_ bv1 1) (_ bv0 1))))
(assert (= p154 (or p150 (= (_ bv0 384) x151))))
(assert (= x153 (bvor x149 x152)))
(assert (= x152 (ite (= (_ bv0 384) x151) (_ bv1 1) (_ bv0 1))))
(assert (= x151 ((_ extract 1151 768) x105)))
(assert (= p150 (not (= x61 x62))))
(assert (= x149 (bvnot x63)))
(assert (= p148 (not (= x56 x57))))
(assert (= x147 (bvnot x58)))
(assert (= x146 (ite (= x56 x57) (_ bv1 1) (_ bv0 1))))
(assert (= p145 (or p78 p143)))
(assert (= x144 (bvor x77 x142)))
(assert (= p143 (and p120 p141)))
(assert (= x142 (bvand x119 x140)))
(assert (= p141 (or p122 p139)))
(assert (= x140 (bvor x121 x138)))
(assert (= p139 (and p132 p137)))
(assert (= x138 (bvand x131 x136)))
(assert (= p137 (or (= x56 x57) (= x134 (_ bv0 384)))))
(assert (= x136 (bvor x133 x135)))
(assert (= x135 (ite (= x134 (_ bv0 384)) (_ bv1 1) (_ bv0 1))))
(assert (= x134 ((_ extract 1151 768) x105)))
(assert (= x133 (ite (= x56 x57) (_ bv1 1) (_ bv0 1))))
(assert (= p132 (or p124 p130)))
(assert (= x131 (bvor x123 x129)))
(assert (= p130 (or (= x61 x62) (= x126 x127))))
(assert (= x129 (bvor x125 x128)))
(assert (= x128 (ite (= x126 x127) (_ bv1 1) (_ bv0 1))))
(assert (= x127 ((_ extract 1151 768) x97)))
(assert (= x126 ((_ extract 1151 768) x105)))
(assert (= x125 (ite (= x61 x62) (_ bv1 1) (_ bv0 1))))
(assert (= p124 (not (= x56 x57))))
(assert (= x123 (bvnot x58)))
(assert (= p122 (and p65 (= x56 x57))))
(assert (= x121 (bvand x64 x66)))
(assert (= p120 (or p83 p118)))
(assert (= x119 (bvor x82 x117)))
(assert (= p118 (and p111 p116)))
(assert (= x117 (bvand x110 x115)))
(assert (= p116 (or (= x56 x57) (= x113 (_ bv0 384)))))
(assert (= x115 (bvor x112 x114)))
(assert (= x114 (ite (= x113 (_ bv0 384)) (_ bv1 1) (_ bv0 1))))
(assert (= x113 ((_ extract 1151 768) x97)))
(assert (= x112 (ite (= x56 x57) (_ bv1 1) (_ bv0 1))))
(assert (= p111 (or p85 p109)))
(assert (= x110 (bvor x84 x108)))
(assert (= p109 (or p87 (= x98 x106))))
(assert (= x108 (bvor x86 x107)))
(assert (= x107 (ite (= x98 x106) (_ bv1 1) (_ bv0 1))))
(assert (= x106 ((_ extract 1151 768) x105)))
(assert (= x105 (x96 x103 x104)))
(assert (= x104 (concat x94 x93)))
(assert (= x103 (x102 x99 x100 x101)))
(assert (= x101 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x22 (_ bv11 4)) (select x22 (_ bv10 4))) (select x22 (_ bv9 4))) (select x22 (_ bv8 4))) (select x22 (_ bv7 4))) (select x22 (_ bv6 4))) (select x22 (_ bv5 4))) (select x22 (_ bv4 4))) (select x22 (_ bv3 4))) (select x22 (_ bv2 4))) (select x22 (_ bv1 4))) (select x22 (_ bv0 4)))))
(assert (= x100 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x23 (_ bv11 4)) (select x23 (_ bv10 4))) (select x23 (_ bv9 4))) (select x23 (_ bv8 4))) (select x23 (_ bv7 4))) (select x23 (_ bv6 4))) (select x23 (_ bv5 4))) (select x23 (_ bv4 4))) (select x23 (_ bv3 4))) (select x23 (_ bv2 4))) (select x23 (_ bv1 4))) (select x23 (_ bv0 4)))))
(assert (= x99 (bvneg (_ bv1388124618062372383947042015309946732620727252194336364173 384))))
(assert (= x98 ((_ extract 1151 768) x97)))
(assert (= x97 (x96 x92 x95)))
(assert (= x95 (concat x94 x93)))
(assert (= x94 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x12 (_ bv11 4)) (select x12 (_ bv10 4))) (select x12 (_ bv9 4))) (select x12 (_ bv8 4))) (select x12 (_ bv7 4))) (select x12 (_ bv6 4))) (select x12 (_ bv5 4))) (select x12 (_ bv4 4))) (select x12 (_ bv3 4))) (select x12 (_ bv2 4))) (select x12 (_ bv1 4))) (select x12 (_ bv0 4)))))
(assert (= x93 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x13 (_ bv11 4)) (select x13 (_ bv10 4))) (select x13 (_ bv9 4))) (select x13 (_ bv8 4))) (select x13 (_ bv7 4))) (select x13 (_ bv6 4))) (select x13 (_ bv5 4))) (select x13 (_ bv4 4))) (select x13 (_ bv3 4))) (select x13 (_ bv2 4))) (select x13 (_ bv1 4))) (select x13 (_ bv0 4)))))
(assert (= x92 (x91 x88 x89 x90)))
(assert (= x90 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x22 (_ bv11 4)) (select x22 (_ bv10 4))) (select x22 (_ bv9 4))) (select x22 (_ bv8 4))) (select x22 (_ bv7 4))) (select x22 (_ bv6 4))) (select x22 (_ bv5 4))) (select x22 (_ bv4 4))) (select x22 (_ bv3 4))) (select x22 (_ bv2 4))) (select x22 (_ bv1 4))) (select x22 (_ bv0 4)))))
(assert (= x89 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x23 (_ bv11 4)) (select x23 (_ bv10 4))) (select x23 (_ bv9 4))) (select x23 (_ bv8 4))) (select x23 (_ bv7 4))) (select x23 (_ bv6 4))) (select x23 (_ bv5 4))) (select x23 (_ bv4 4))) (select x23 (_ bv3 4))) (select x23 (_ bv2 4))) (select x23 (_ bv1 4))) (select x23 (_ bv0 4)))))
(assert (= x88 (bvneg (_ bv1388124618062372383947042015309946732620727252194336364173 384))))
(assert (= p87 (not (= x61 x62))))
(assert (= x86 (bvnot x63)))
(assert (= p85 (not (= x56 x57))))
(assert (= x84 (bvnot x58)))
(assert (= p83 (or (= x61 x62) p81)))
(assert (= x82 (bvor x79 x80)))
(assert (= p81 (not (= x56 x57))))
(assert (= x80 (bvnot x58)))
(assert (= x79 (ite (= x61 x62) (_ bv1 1) (_ bv0 1))))
(assert (= p78 (not (= x56 x57))))
(assert (= x77 (bvnot x58)))
(assert (= p76 (or p70 p74)))
(assert (= x75 (bvor x69 x73)))
(assert (= p74 (and (= x61 x62) (= x56 x57))))
(assert (= x73 (bvand x71 x72)))
(assert (= x72 (ite (= x56 x57) (_ bv1 1) (_ bv0 1))))
(assert (= x71 (ite (= x61 x62) (_ bv1 1) (_ bv0 1))))
(assert (= p70 (or p60 p68)))
(assert (= x69 (bvor x59 x67)))
(assert (= p68 (and p65 (= x56 x57))))
(assert (= x67 (bvand x64 x66)))
(assert (= x66 (ite (= x56 x57) (_ bv1 1) (_ bv0 1))))
(assert (= p65 (not (= x61 x62))))
(assert (= x64 (bvnot x63)))
(assert (= x63 (ite (= x61 x62) (_ bv1 1) (_ bv0 1))))
(assert (= x62 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x10 (_ bv11 4)) (select x10 (_ bv10 4))) (select x10 (_ bv9 4))) (select x10 (_ bv8 4))) (select x10 (_ bv7 4))) (select x10 (_ bv6 4))) (select x10 (_ bv5 4))) (select x10 (_ bv4 4))) (select x10 (_ bv3 4))) (select x10 (_ bv2 4))) (select x10 (_ bv1 4))) (select x10 (_ bv0 4)))))
(assert (= x61 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x12 (_ bv11 4)) (select x12 (_ bv10 4))) (select x12 (_ bv9 4))) (select x12 (_ bv8 4))) (select x12 (_ bv7 4))) (select x12 (_ bv6 4))) (select x12 (_ bv5 4))) (select x12 (_ bv4 4))) (select x12 (_ bv3 4))) (select x12 (_ bv2 4))) (select x12 (_ bv1 4))) (select x12 (_ bv0 4)))))
(assert (= p60 (not (= x56 x57))))
(assert (= x59 (bvnot x58)))
(assert (= x58 (ite (= x56 x57) (_ bv1 1) (_ bv0 1))))
(assert (= x57 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x11 (_ bv11 4)) (select x11 (_ bv10 4))) (select x11 (_ bv9 4))) (select x11 (_ bv8 4))) (select x11 (_ bv7 4))) (select x11 (_ bv6 4))) (select x11 (_ bv5 4))) (select x11 (_ bv4 4))) (select x11 (_ bv3 4))) (select x11 (_ bv2 4))) (select x11 (_ bv1 4))) (select x11 (_ bv0 4)))))
(assert (= x56 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x13 (_ bv11 4)) (select x13 (_ bv10 4))) (select x13 (_ bv9 4))) (select x13 (_ bv8 4))) (select x13 (_ bv7 4))) (select x13 (_ bv6 4))) (select x13 (_ bv5 4))) (select x13 (_ bv4 4))) (select x13 (_ bv3 4))) (select x13 (_ bv2 4))) (select x13 (_ bv1 4))) (select x13 (_ bv0 4)))))
(assert true)
(assert (= (select x55 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x55 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x55 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x55 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x54 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x54 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x54 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x54 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x53 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x53 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x53 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x53 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x52 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x52 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x52 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x52 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x51 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x51 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x51 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x51 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x51 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x51 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x51 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x51 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x50 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x50 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x50 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x50 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x49 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x49 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x49 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x49 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x48 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x48 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x48 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x48 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x47 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x47 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x47 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x47 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x46 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x46 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x46 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x46 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x46 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x46 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x46 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x46 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x45 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x45 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x45 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x45 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x45 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x45 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x45 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x45 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x44 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x44 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x44 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x44 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x44 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x44 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x44 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x44 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x43 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x43 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x43 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x43 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x43 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x43 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x43 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x43 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x42 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x42 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x42 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x42 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x42 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x42 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x42 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x42 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x41 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x41 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x41 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x41 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x41 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x41 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x41 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x41 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x40 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x40 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x40 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x40 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x40 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x40 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x40 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x40 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x39 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x39 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x39 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x39 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x39 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x39 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x39 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x39 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x38 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x38 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x38 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x38 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x38 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x38 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x38 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x38 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x37 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x37 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x37 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x37 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x37 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x37 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x37 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x37 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x36 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x36 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x36 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x36 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x36 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x36 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x36 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x36 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x35 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x35 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x35 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x35 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x34 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x34 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x34 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x34 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x33 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x33 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x33 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x33 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x32 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x32 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x32 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x32 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x32 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x32 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x32 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x32 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x31 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x31 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x31 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x31 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x30 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x30 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x30 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x30 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x29 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x29 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x29 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x29 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x28 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x28 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x28 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x28 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x28 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x28 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x28 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x28 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x27 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x27 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x27 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x27 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x26 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x26 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x26 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x26 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x25 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x25 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x25 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x25 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x24 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x24 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x24 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x24 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x24 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x24 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x24 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x24 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x23 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x23 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x23 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x23 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x22 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x22 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x22 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x22 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x21 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x21 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x21 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x21 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x20 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x20 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x20 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x20 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x19 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x19 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x19 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x19 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x18 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x18 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x18 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x18 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x17 (_ bv31 5)) (_ bv0 32)))
(assert (= (select x17 (_ bv30 5)) (_ bv0 32)))
(assert (= (select x17 (_ bv29 5)) (_ bv0 32)))
(assert (= (select x17 (_ bv28 5)) (_ bv0 32)))
(assert (= (select x17 (_ bv27 5)) (_ bv0 32)))
(assert (= (select x17 (_ bv26 5)) (_ bv0 32)))
(assert (= (select x17 (_ bv25 5)) (_ bv0 32)))
(assert (= (select x17 (_ bv24 5)) (_ bv0 32)))
(assert (= (select x16 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x16 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x16 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x16 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x15 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x15 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x15 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x15 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x14 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x14 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x14 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x14 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x13 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x13 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x13 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x13 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x12 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x12 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x12 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x12 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x11 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x11 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x11 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x11 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x10 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x10 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x10 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x10 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x9 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x9 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x9 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x9 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x8 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x8 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x8 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x8 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x7 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x7 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x7 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x7 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x6 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x6 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x6 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x6 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x5 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x5 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x5 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x5 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x4 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x4 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x4 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x4 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x3 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x3 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x3 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x3 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x2 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x2 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x2 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x2 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv12 4)) (_ bv0 32)))
(assert (= (select x0 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x0 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x0 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x0 (_ bv12 4)) (_ bv0 32)))
(assert (not (=> p76 p167)))
(check-sat)
(exit)
